#include "RobotLogic.h"

void Substitute::add(LogicExpression* oldExpr,LogicExpression* newExpr)
{
	SubstitutePair sub;
	sub.oldExpr = oldExpr;
	string name = newExpr->getName();
	LogicExpression* val;
	if(newExpr->isFunc() && name.compare("DEC")==0 )
	{

		LogicExpression* arg = ((FuncExpression*)newExpr)->getSingleArgument();
		if(arg->isConst())
		{
			val = new ConstExpression(((ConstExpression*)arg)->getValue()-1);
		}

	}
	else if(newExpr->isFunc() && name.compare("INC")==0 )
	{

		LogicExpression* arg = ((FuncExpression*)newExpr)->getSingleArgument();
		if(arg->isConst())
		{
			val = new ConstExpression(((ConstExpression*)arg)->getValue()+1);
		}

	}
	else
	{
		val=newExpr;
	}
	sub.newExpr = val;
	listSubstitutePairs.push_back(sub);
}
int Substitute::find(LogicExpression *expr)
{
	for(int i=0;i<listSubstitutePairs.size();i++)
	{
		if(expr->isEqual(listSubstitutePairs[i].oldExpr))
		{
			return i;
		}
	}
	return -1;
}
Substitute Substitute::unifyVar(LogicExpression* var, LogicExpression* x, Substitute& s)
{
	int k = 0;
	if(k = s.find(var)>-1)
	{
		return unify(s.listSubstitutePairs[k].newExpr,x,s);
	}
	else if(k = s.find(x)>-1)
	{
		return unify(var,s.listSubstitutePairs[k].newExpr,s);
	}
	else if(x->contain(var))
	{
		s.flag = false;
		return s;
	}
	LogicExpression*temp=var;
	temp = x;
	s.add(var,x);
	return s;
}

Substitute Substitute::unify(LogicExpression* x, LogicExpression* y, Substitute& s)
{
	if(s.isFalse())
	{
		return s;
	}
	else if(x->isEqual(y))
	{
		return s;
	}
	else if(x->isVar())
	{
		return unifyVar(x,y,s);
	}
	else if(y->isVar())
	{
		return unifyVar(y,x,s);
	}
	else if(x->isFunc())
	{
		LogicExpression* lx = ((FuncExpression*)x)->getArguments();
		if(y->isFunc() && x->getName().compare(y->getName()) == 0)  
		{
			
			LogicExpression* ly = ((FuncExpression*)y)->getArguments();
			return unify(lx,ly,s);
		}
		else if(x->getName().compare("DEC") == 0 && y->isConst())
		{
			vector<LogicExpression*> argument(1);
			argument[0] = new ConstExpression(((ConstExpression*)y)->getValue()+1);
			return unify(lx,new ListExpression(argument),s);
		}
		else if(x->getName().compare("INC") == 0 && y->isConst())
		{
			vector<LogicExpression*> argument(1);
			argument[0] = new ConstExpression(((ConstExpression*)y)->getValue()-1);
			return unify(lx,new ListExpression(argument),s);
		}
		else
		{
			s.flag = false;
			return s;
		}
	}
	else if(x->isList() && y->isList())
	{
		s = unify(((ListExpression*)x)->popFirst(),((ListExpression*)y)->popFirst(),s);
		return unify(x,y,s);
	}
	s.flag = false;
	return s;
}

LogicExpression* RobotLogic::string2Expression(string str)
{
	if(str.length() == 0)
	{
		vector<LogicExpression*> temp;
		return new ListExpression(temp);
	}
	int end =0;
	int start = 0;
	start = str.find_first_of("(") ;
	if(start >0)
	{
		end = str.find_last_of(")") ;
		string funcName = str.substr(0,start);
				
		FuncExpression* expr = new FuncExpression(funcName);
		expr->setlistArguments(string2ListExpressions(str.substr(start+1,end-start-1)) );
		return expr;
	}
	else if((str[0]>='0' && str[0]<='9') || str[0]=='-')
	{
		ConstExpression* expr = new ConstExpression(atoi(str.c_str()));
		return expr;
	}
	else
	{
		VarExpression* expr = new VarExpression(str);
		return expr;
	}

}
vector<LogicExpression*> RobotLogic::string2ListExpressions(string str)
{
	vector<LogicExpression*> list;
	int k =0;
	int start = 0;
	int open = 0;
	k= str.find_first_of(",()");
	while(k >-1)
	{
		switch(str[k])
		{
		case ',':
			if(open ==0)
			{
				string strSingleExpr = str.substr(start,k-start);
				start = k+1;
				list.push_back(string2Expression(strSingleExpr));
			}
			break;
		case '(':
			open++;
			break;
		case ')':
			open--;
			break;
		}
		k= str.find_first_of(",()",k+1);
	}
	string strSingleExpr = str.substr(start);
	list.push_back(string2Expression(strSingleExpr));
	return list;
}


RobotLogic::RobotLogic(void)
{
}
void RobotLogic::loadKB(char* filename)
{
	ifstream file(filename);
	
	while(!file.eof())
	{
		char buffer[256];
		file.getline(buffer,256);
		string str(buffer);

		int c1 = str.find("IF ");
		int c2 = str.find(" THEN ");
		if(c1<c2 && c1 >= 0 && c2+6 < str.length())
		{
			HornClause horn;
			string clause1 = str.substr(c1+3,c2-c1-3);
			
			int k =0;
			int n =clause1.find(" AND ");
			while(n != -1)
			{
				string temp = clause1.substr(0,n);
				k=n+5;
				clause1 = clause1.substr(k);
				n =clause1.find(" AND ");
				
				horn.negativeLiterals.push_back( string2Expression(temp));
			}
			
			horn.negativeLiterals.push_back( string2Expression(clause1));
			string clause2 = str.substr(c2+6);
			horn.setPositiveLiteral(string2Expression(clause2));
			KB.push_back(horn);

		}
	}

	file.close();
}
void RobotLogic::addSingleExpression(LogicExpression* e)
{
	for(int i = 0;i<singleExpressions.size();i++)
	{
		if(e->isEqual(singleExpressions[i]))
		{
			return ;
		}
	}
	singleExpressions.push_back(e);
}
void RobotLogic::addSingleExpression(string exprString)
{
	LogicExpression* e = string2Expression(exprString);
	addSingleExpression(e);
}
bool RobotLogic::FOL_FC_Ask(string alphaString)
{
	LogicExpression* alpha = string2Expression(alphaString);
	return FOL_FC_Ask(alpha);
}

bool RobotLogic::FOL_FC_Ask(LogicExpression* alpha)
{
	for(int i = 0;i<singleExpressions.size();i++)
	{
		if(alpha->isEqual(singleExpressions[i]))
		{
			return true;
		}
	}
	int count=0;
	do
	{
		count=0;
		
		for(int i=0;i<KB.size();i++)
		{
			for(int j=0;j<singleExpressions.size();j++)
			{
				Substitute sub;
				LogicExpression* x = KB[i].negativeLiterals[0];
				sub = sub.unify(x,singleExpressions[j],sub);
				if(!sub.isFalse())
				{

					int k;
					for( k = 1;k<KB[i].negativeLiterals.size();k++)
					{


						LogicExpression* p = KB[i].negativeLiterals[k];
						p = p->applySubstitute(&sub);



						bool flag = false;
						for(int l = 0;l<singleExpressions.size();l++)
						{				
							LogicExpression* q = singleExpressions[l]->applySubstitute(&sub);
					
							if(p->isEqual(q))
							{
								flag = true;
								break;
							}
							
						}
						if(!flag)
						{
							break;
						}
					}
					
					if(k == KB[i].negativeLiterals.size())
					{
						LogicExpression* newExpr =  KB[i].getPositiveLiteral()->applySubstitute(&sub);
						bool flag = true;

						for(int l = 0;l<singleExpressions.size();l++)
						{
							if(newExpr->isEqual(singleExpressions[l]))
							{
								flag = false;
								break;
							}
						}
						if(flag)
						{
							singleExpressions.push_back(newExpr);
							if(alpha->isEqual(newExpr))
							{
								return true;
							}
							count++;
						}
					}

				}
			}
		}
	}
	while(count>0);
	return false;
}
RobotLogic::~RobotLogic(void)
{
}
